\begin{tabbing}
$\forall$\=$A$:Type, ${\it eq}$:EqDecider($A$), ${\it df}$:$x$:$A$ fp$\rightarrow$ Type, $f$:$x$:$A$ fp$\rightarrow$ ${\it df}$($x$)?Top, ${\it dg}$:$x$:$A$ fp$\rightarrow$ Type,\+
\\[0ex]$g$:$x$:$A$ fp$\rightarrow$ ${\it dg}$($x$)?Top.
\-\\[0ex]${\it df}$ $\parallel$ ${\it dg}$
\\[0ex]$\Rightarrow$ ($\forall$$x$:$A$. $x$ $\in$ dom($f$) $\Rightarrow$ $x$ $\in$ dom(${\it df}$))
\\[0ex]$\Rightarrow$ ($\forall$$x$:$A$. $x$ $\in$ dom($g$) $\Rightarrow$ $x$ $\in$ dom(${\it dg}$))
\\[0ex]$\Rightarrow$ $f$ $\oplus$ $g$ $\in$ $x$:$A$ fp$\rightarrow$ ${\it df}$ $\oplus$ ${\it dg}$($x$)?Top
\end{tabbing}